\section{A difficult family of properties}
\label{sec:takelenrev}

In this section we discuss a family of properties that are easy for a human to prove but which seem to be a significant obstacle to automated inductive theorem proving. This family includes the first five failed proofs in Section \ref{sec:unprovable} but can be more easily categorised by the following property (a sub-proof needed for the first from the list of failures):

\begin{center}
\li{take (len xs)} \li{(rev xs)} \li{= take (len xs)} \li{(concat (rev xs)} \li{(Cons x Nil))}
\end{center}

Here the \li{take :: Nat -> List -> List} function takes a \li{Nat} argument \li{n} and a \li{List} argument \li{xs} and returns the first \li{n} elements of the list \li{xs}. \li{rev :: List -> List} takes a list and reverses it, \li{len :: List -> Nat} returns the length of a list and \li{concat :: List -> List -> List} takes two lists and concatenates them. The formal definition of these functions can be found in Appendix \ref{app:fundefs}.

What this property is saying is that if we take the length of a list from the reverse of that list it is the same as taking this number of elements from the same reversed list, but with some new element added to the end. This is obviously the case since the \li{take} function will drop this last element from the end as it is only taking the number of elements in the original list.

A human would understand what is \emph{meant} by the various functions and knows that reversing a list does not affect its length. By proving this formally, i.e. \li{len xs = len (rev xs)}, they could therefore reduce the proof to the much easier one below:

\begin{center}
\li{take (len xs)} \li{xs} \li{= take (len xs)} \li{(concat xs} \li{(Cons x Nil))}
\end{center}

Both this property, and the lemma \li{len xs = len (rev xs)} required to produce it are easy for Zeno to prove. The difficulty comes in being able to infer this lemma from the original problem. There are some properties Zeno cannot currently prove which we feel will be provable with further research and enough computation power, such as verifying a sorting algorithm (\li{sorted (sort xs) = True}). We have however yet to find an automated technique which could attempt the proof given here. It might be the case that these proofs are ones which require a human level intelligence to provide auxiliary lemmas in order to complete them.